Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    a__fst(0,Z)  → nil
2:    a__fst(s(X),cons(Y,Z))  → cons(mark(Y),fst(X,Z))
3:    a__from(X)  → cons(mark(X),from(s(X)))
4:    a__add(0,X)  → mark(X)
5:    a__add(s(X),Y)  → s(add(X,Y))
6:    a__len(nil)  → 0
7:    a__len(cons(X,Z))  → s(len(Z))
8:    mark(fst(X1,X2))  → a__fst(mark(X1),mark(X2))
9:    mark(from(X))  → a__from(mark(X))
10:    mark(add(X1,X2))  → a__add(mark(X1),mark(X2))
11:    mark(len(X))  → a__len(mark(X))
12:    mark(0)  → 0
13:    mark(s(X))  → s(X)
14:    mark(nil)  → nil
15:    mark(cons(X1,X2))  → cons(mark(X1),X2)
16:    a__fst(X1,X2)  → fst(X1,X2)
17:    a__from(X)  → from(X)
18:    a__add(X1,X2)  → add(X1,X2)
19:    a__len(X)  → len(X)
There are 14 dependency pairs:
20:    A__FST(s(X),cons(Y,Z))  → MARK(Y)
21:    A__FROM(X)  → MARK(X)
22:    A__ADD(0,X)  → MARK(X)
23:    MARK(fst(X1,X2))  → A__FST(mark(X1),mark(X2))
24:    MARK(fst(X1,X2))  → MARK(X1)
25:    MARK(fst(X1,X2))  → MARK(X2)
26:    MARK(from(X))  → A__FROM(mark(X))
27:    MARK(from(X))  → MARK(X)
28:    MARK(add(X1,X2))  → A__ADD(mark(X1),mark(X2))
29:    MARK(add(X1,X2))  → MARK(X1)
30:    MARK(add(X1,X2))  → MARK(X2)
31:    MARK(len(X))  → A__LEN(mark(X))
32:    MARK(len(X))  → MARK(X)
33:    MARK(cons(X1,X2))  → MARK(X1)
The approximated dependency graph contains one SCC: {20-30,32,33}.
Tyrolean Termination Tool  (1.04 seconds)   ---  May 3, 2006